let P1, P2 be AntiChain_of_Prefixes of dom (tree_of_subformulae F); :: thesis: ( ( for t being Element of dom (tree_of_subformulae F) holds
( t in P1 iff (tree_of_subformulae F) . t = G ) ) & ( for t being Element of dom (tree_of_subformulae F) holds
( t in P2 iff (tree_of_subformulae F) . t = G ) ) implies P1 = P2 )
assume A6: for t being Element of dom (tree_of_subformulae F) holds
( t in P1 iff (tree_of_subformulae F) . t = G ) ; :: thesis: ( ex t being Element of dom (tree_of_subformulae F) st
( ( t in P2 implies (tree_of_subformulae F) . t = G ) implies ( (tree_of_subformulae F) . t = G & not t in P2 ) ) or P1 = P2 )
assume A7: for t being Element of dom (tree_of_subformulae F) holds
( t in P2 iff (tree_of_subformulae F) . t = G ) ; :: thesis: P1 = P2
thus P1 c= P2 :: according to XBOOLE_0:def 10 :: thesis: P2 c= P1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 or x in P2 )
assume A8: x in P1 ; :: thesis: x in P2
P1 c= dom (tree_of_subformulae F) by TREES_1:def 11;
then reconsider t = x as Element of dom (tree_of_subformulae F) by A8;
(tree_of_subformulae F) . t = G by A6, A8;
hence x in P2 by A7; :: thesis: verum
end;
thus P2 c= P1 :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P2 or x in P1 )
assume A9: x in P2 ; :: thesis: x in P1
P2 c= dom (tree_of_subformulae F) by TREES_1:def 11;
then reconsider t = x as Element of dom (tree_of_subformulae F) by A9;
(tree_of_subformulae F) . t = G by A7, A9;
hence x in P1 by A6; :: thesis: verum
end;