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
A2: ( ( 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} )
A3: 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 A4: y in W ; :: thesis: y in W \ {x}
then not y in {x} by A1, A2, TARSKI:def 1;
hence y in W \ {x} by A4, XBOOLE_0:def 5; :: thesis: verum

end;

for y being set st y in W \ {x} holds
y in W by XBOOLE_0:def 5;
then W \ {x} = W by A3, TARSKI:2;
hence ( x in W1 & W c= W1 \ {x} ) by A1, A2, XBOOLE_1:33; :: thesis: verum

end;

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