let H be LTL-formula; :: thesis: for W, W1 being Subset of (Subformulae H) holds
( not W c= W1 or W = W1 or ex x being set st
( x in W1 & W c= W1 \ {x} ) )
let W, W1 be Subset of (Subformulae H); :: thesis: ( not W c= W1 or W = W1 or ex x being set st
( x in W1 & W c= W1 \ {x} ) )
assume A1: W c= W1 ; :: thesis: ( W = W1 or ex x being set st
( x in W1 & W c= W1 \ {x} ) )
( not W = W1 implies ex x being set st
( x in W1 & W c= W1 \ {x} ) )

proof

assume not W = W1 ; :: thesis: ex x being set st
( x in W1 & W c= W1 \ {x} )
then consider x being set such that
B1: ( ( x in W & not x in W1 ) or ( x in W1 & not x in W ) ) by TARSKI:2;
take x ; :: thesis: ( x in W1 & W c= W1 \ {x} )
W \ {x} = W

proof

C1: for y being set st y in W \ {x} holds
y in W by XBOOLE_0:def 5;
for y being set st y in W holds
y in W \ {x}

proof

let y be set ; :: thesis: ( y in W implies y in W \ {x} )
assume y in W ; :: thesis: y in W \ {x}
then ( y in W & not y in {x} ) by A1, B1, TARSKI:def 1;
hence y in W \ {x} by XBOOLE_0:def 5; :: thesis: verum

end;

hence W \ {x} = W by C1, TARSKI:2; :: thesis: verum

end;

hence ( x in W1 & W c= W1 \ {x} ) by A1, B1, XBOOLE_1:33; :: thesis: verum

end;

hence ( W = W1 or ex x being set st
( x in W1 & W c= W1 \ {x} ) ) ; :: thesis: verum