let L be non empty RelStr ; :: thesis: for X, Y being set st ( for x being Element of L holds
( x is_<=_than X iff x is_<=_than Y ) ) & ex_inf_of X,L holds
ex_inf_of Y,L
let X, Y be set ; :: thesis: ( ( for x being Element of L holds
( x is_<=_than X iff x is_<=_than Y ) ) & ex_inf_of X,L implies ex_inf_of Y,L )
assume A1: for x being Element of L holds
( x is_<=_than X iff x is_<=_than Y ) ; :: thesis: ( not ex_inf_of X,L or ex_inf_of Y,L )
given a being Element of L such that A2: X is_>=_than a and
A3: for b being Element of L st X is_>=_than b holds
a >= b and
A4: for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds
c >= b ) holds
c = a ; :: according to YELLOW_0:def 8 :: thesis: ex_inf_of Y,L
take a ; :: according to YELLOW_0:def 8 :: thesis: ( Y is_>=_than a & ( for b being Element of L st Y is_>=_than b holds
b <= a ) & ( for c being Element of L st Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds
b <= c ) holds
c = a ) )
thus Y is_>=_than a by A1, A2; :: thesis: ( ( for b being Element of L st Y is_>=_than b holds
b <= a ) & ( for c being Element of L st Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds
b <= c ) holds
c = a ) )

hereby :: thesis: for c being Element of L st Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds
b <= c ) holds
c = a

let b be Element of L; :: thesis: ( Y is_>=_than b implies a >= b )
assume Y is_>=_than b ; :: thesis: a >= b
then X is_>=_than b by A1;
hence a >= b by A3; :: thesis: verum

end;

let c be Element of L; :: thesis: ( Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds
b <= c ) implies c = a )
assume Y is_>=_than c ; :: thesis: ( ex b being Element of L st
( Y is_>=_than b & not b <= c ) or c = a )
then A5: X is_>=_than c by A1;
assume A6: for b being Element of L st Y is_>=_than b holds
c >= b ; :: thesis: c = a

now

let b be Element of L; :: thesis: ( X is_>=_than b implies c >= b )
assume X is_>=_than b ; :: thesis: c >= b
then Y is_>=_than b by A1;
hence c >= b by A6; :: thesis: verum

end;

hence c = a by A4, A5; :: thesis: verum