consider X being set such that
A1: X = { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } ;
A2: for t being Element of dom (tree_of_subformulae F) holds
( t in X iff (tree_of_subformulae F) . t = G )

proof

let t be Element of dom (tree_of_subformulae F); :: thesis: ( t in X iff (tree_of_subformulae F) . t = G )
thus ( t in X iff (tree_of_subformulae F) . t = G ) :: thesis: verum

proof

now

assume t in X ; :: thesis: (tree_of_subformulae F) . t = G
then consider t' being Element of dom (tree_of_subformulae F) such that
A3: ( t' = t & (tree_of_subformulae F) . t' = G ) by A1;
thus (tree_of_subformulae F) . t = G by A3; :: thesis: verum

end;

hence ( t in X implies (tree_of_subformulae F) . t = G ) ; :: thesis: ( (tree_of_subformulae F) . t = G implies t in X )
assume (tree_of_subformulae F) . t = G ; :: thesis: t in X
hence t in X by A1; :: thesis: verum

end;

end;

X is AntiChain_of_Prefixes of dom (tree_of_subformulae F)

proof

A4: for x being set st x in X holds
x is FinSequence

proof

let x be set ; :: thesis: ( x in X implies x is FinSequence )
assume x in X ; :: thesis: x is FinSequence
then consider t being Element of dom (tree_of_subformulae F) such that
A5: ( t = x & (tree_of_subformulae F) . t = G ) by A1;
thus x is FinSequence by A5; :: thesis: verum

end;

for p1, p2 being FinSequence st p1 in X & p2 in X & p1 <> p2 holds
not p1,p2 are_c=-comparable

proof

let p1, p2 be FinSequence; :: thesis: ( p1 in X & p2 in X & p1 <> p2 implies not p1,p2 are_c=-comparable )
assume A6: ( p1 in X & p2 in X & p1 <> p2 ) ; :: thesis: not p1,p2 are_c=-comparable
then consider t1 being Element of dom (tree_of_subformulae F) such that
A7: ( t1 = p1 & (tree_of_subformulae F) . t1 = G ) by A1;
consider t2 being Element of dom (tree_of_subformulae F) such that
A8: ( t2 = p2 & (tree_of_subformulae F) . t2 = G ) by A1, A6;
thus not p1,p2 are_c=-comparable by A6, A7, A8, Th47; :: thesis: verum

end;

then reconsider X = X as AntiChain_of_Prefixes by A4, TREES_1:def 13;
X c= dom (tree_of_subformulae F)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom (tree_of_subformulae F) )
assume x in X ; :: thesis: x in dom (tree_of_subformulae F)
then consider t being Element of dom (tree_of_subformulae F) such that
A9: ( t = x & (tree_of_subformulae F) . t = G ) by A1;
thus x in dom (tree_of_subformulae F) by A9; :: thesis: verum

end;

hence X is AntiChain_of_Prefixes of dom (tree_of_subformulae F) by TREES_1:def 14; :: thesis: verum

end;

hence ex b₁ being AntiChain_of_Prefixes of dom (tree_of_subformulae F) st
for t being Element of dom (tree_of_subformulae F) holds
( t in b₁ iff (tree_of_subformulae F) . t = G ) by A2; :: thesis: verum