let L be non empty doubleLoopStr ; :: thesis: for F being non empty Subset of L st F <> {(0. L)} holds
ex x being Element of L st
( x <> 0. L & x in F )
let F be non empty Subset of L; :: thesis: ( F <> {(0. L)} implies ex x being Element of L st
( x <> 0. L & x in F ) )
assume A1: F <> {(0. L)} ; :: thesis: ex x being Element of L st
( x <> 0. L & x in F )
now :: thesis: ex x being set st
( x in F & not x = 0. L )
assume A2: for x being set st x in F holds
x = 0. L ; :: thesis: contradiction
for x being object holds
( x in F iff x = 0. L )
proof
let e be object ; :: thesis: ( e in F iff e = 0. L )
A3: ex a being object st a in F by XBOOLE_0:def 1;
thus ( e in F implies e = 0. L ) by A2; :: thesis: ( e = 0. L implies e in F )
assume e = 0. L ; :: thesis: e in F
hence e in F by A2, A3; :: thesis: verum
end;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum
end;
hence ex x being Element of L st
( x <> 0. L & x in F ) ; :: thesis: verum