let L be non empty RelStr ; :: thesis: for X being set
for x being Element of L holds
( ( x is_>=_than X implies x is_>=_than X /\ the carrier of L ) & ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) )
let X be set ; :: thesis: for x being Element of L holds
( ( x is_>=_than X implies x is_>=_than X /\ the carrier of L ) & ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) )
let x be Element of L; :: thesis: ( ( x is_>=_than X implies x is_>=_than X /\ the carrier of L ) & ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) )
set Y = X /\ the carrier of L;
thus ( X is_<=_than x implies X /\ the carrier of L is_<=_than x ) :: thesis: ( ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) )

proof

assume A1: for b being Element of L st b in X holds
b <= x ; :: according to LATTICE3:def 9 :: thesis: X /\ the carrier of L is_<=_than x
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in X /\ the carrier of L or b <= x )
assume b in X /\ the carrier of L ; :: thesis: b <= x
then b in X by XBOOLE_0:def 4;
hence b <= x by A1; :: thesis: verum

end;

thus ( X /\ the carrier of L is_<=_than x implies X is_<=_than x ) :: thesis: ( x is_<=_than X iff x is_<=_than X /\ the carrier of L )

proof

assume A2: for b being Element of L st b in X /\ the carrier of L holds
b <= x ; :: according to LATTICE3:def 9 :: thesis: X is_<=_than x
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in X or b <= x )
assume b in X ; :: thesis: b <= x
then b in X /\ the carrier of L by XBOOLE_0:def 4;
hence b <= x by A2; :: thesis: verum

end;

thus ( X is_>=_than x implies X /\ the carrier of L is_>=_than x ) :: thesis: ( x is_<=_than X /\ the carrier of L implies x is_<=_than X )

proof

assume A3: for b being Element of L st b in X holds
b >= x ; :: according to LATTICE3:def 8 :: thesis: X /\ the carrier of L is_>=_than x
let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in X /\ the carrier of L or x <= b )
assume b in X /\ the carrier of L ; :: thesis: x <= b
then b in X by XBOOLE_0:def 4;
hence x <= b by A3; :: thesis: verum

end;

thus ( X /\ the carrier of L is_>=_than x implies X is_>=_than x ) :: thesis: verum

proof

assume A4: for b being Element of L st b in X /\ the carrier of L holds
b >= x ; :: according to LATTICE3:def 8 :: thesis: X is_>=_than x
let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in X or x <= b )
assume b in X ; :: thesis: x <= b
then b in X /\ the carrier of L by XBOOLE_0:def 4;
hence x <= b by A4; :: thesis: verum

end;