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: X is AntiChain_of_Prefixes of dom (tree_of_subformulae F)

proof

A3: 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 that
A4: ( p1 in X & p2 in X ) and
A5: p1 <> p2 ; :: thesis: not p1,p2 are_c=-comparable
( ex t1 being Element of dom (tree_of_subformulae F) st
( t1 = p1 & (tree_of_subformulae F) . t1 = G ) & ex t2 being Element of dom (tree_of_subformulae F) st
( t2 = p2 & (tree_of_subformulae F) . t2 = G ) ) by A1, A4;
hence not p1,p2 are_c=-comparable by A5, Th18; :: thesis: verum

end;

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 ex t being Element of dom (tree_of_subformulae F) st
( t = x & (tree_of_subformulae F) . t = G ) by A1;
hence x is FinSequence ; :: thesis: verum

end;

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

proof

let x be object ; :: 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 ex t being Element of dom (tree_of_subformulae F) st
( t = x & (tree_of_subformulae F) . t = G ) by A1;
hence x in dom (tree_of_subformulae F) ; :: thesis: verum

end;

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

end;

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 :: thesis: ( t in X implies (tree_of_subformulae F) . t = G )

assume t in X ; :: thesis: (tree_of_subformulae F) . t = G
then ex t9 being Element of dom (tree_of_subformulae F) st
( t9 = t & (tree_of_subformulae F) . t9 = G ) by A1;
hence (tree_of_subformulae F) . t = G ; :: 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;

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