let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of L

for x being Element of L holds

( x is_>=_than X iff x is_>=_than downarrow X )

let X be Subset of L; :: thesis: for x being Element of L holds

( x is_>=_than X iff x is_>=_than downarrow X )

let x be Element of L; :: thesis: ( x is_>=_than X iff x is_>=_than downarrow X )

thus ( x is_>=_than X implies x is_>=_than downarrow X ) :: thesis: ( x is_>=_than downarrow X implies x is_>=_than X )

x >= y ; :: according to LATTICE3:def 9 :: thesis: x is_>=_than X

let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in X or y <= x )

assume A5: y in X ; :: thesis: y <= x

y <= y ;

then y in downarrow X by A5, Def15;

hence y <= x by A4; :: thesis: verum

for x being Element of L holds

( x is_>=_than X iff x is_>=_than downarrow X )

let X be Subset of L; :: thesis: for x being Element of L holds

( x is_>=_than X iff x is_>=_than downarrow X )

let x be Element of L; :: thesis: ( x is_>=_than X iff x is_>=_than downarrow X )

thus ( x is_>=_than X implies x is_>=_than downarrow X ) :: thesis: ( x is_>=_than downarrow X implies x is_>=_than X )

proof

assume A4:
for y being Element of L st y in downarrow X holds
assume A1:
for y being Element of L st y in X holds

x >= y ; :: according to LATTICE3:def 9 :: thesis: x is_>=_than downarrow X

let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in downarrow X or y <= x )

assume y in downarrow X ; :: thesis: y <= x

then consider z being Element of L such that

A2: y <= z and

A3: z in X by Def15;

x >= z by A1, A3;

hence y <= x by A2, ORDERS_2:3; :: thesis: verum

end;x >= y ; :: according to LATTICE3:def 9 :: thesis: x is_>=_than downarrow X

let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in downarrow X or y <= x )

assume y in downarrow X ; :: thesis: y <= x

then consider z being Element of L such that

A2: y <= z and

A3: z in X by Def15;

x >= z by A1, A3;

hence y <= x by A2, ORDERS_2:3; :: thesis: verum

x >= y ; :: according to LATTICE3:def 9 :: thesis: x is_>=_than X

let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in X or y <= x )

assume A5: y in X ; :: thesis: y <= x

y <= y ;

then y in downarrow X by A5, Def15;

hence y <= x by A4; :: thesis: verum