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 ) )
thus for b being Element of L st Y is_>=_than b holds
a >= b by A1, A3; :: 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 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 A5: Y is_>=_than c ; :: thesis: ( ex b being Element of L st
( Y is_>=_than b & not b <= c ) or c = a )
assume A6: for b being Element of L st Y is_>=_than b holds
c >= b ; :: thesis: c = a
A7: for b being Element of L st X is_>=_than b holds
c >= b by A1, A6;
X is_>=_than c by A1, A5;
hence c = a by A4, A7; :: thesis: verum