(∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
(∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) →
Q G1 L1 T1
) →
∀G,L,T. ≥𝐒 ❪G,L,T❫ → Q G L T.
#Q #IH #G #L #T #H elim H -G -L -T
(∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
(∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) →
Q G1 L1 T1
) →
∀G,L,T. ≥𝐒 ❪G,L,T❫ → Q G L T.
#Q #IH #G #L #T #H elim H -G -L -T