let L be non empty transitive RelStr ; :: thesis: for S being non empty full SubRelStr of L
for X being Subset of S st ex_inf_of X,L & "/\" X,L in the carrier of S holds
( ex_inf_of X,S & "/\" X,S = "/\" X,L )
let S be non empty full SubRelStr of L; :: thesis: for X being Subset of S st ex_inf_of X,L & "/\" X,L in the carrier of S holds
( ex_inf_of X,S & "/\" X,S = "/\" X,L )
let X be Subset of S; :: thesis: ( ex_inf_of X,L & "/\" X,L in the carrier of S implies ( ex_inf_of X,S & "/\" X,S = "/\" X,L ) )
assume that
A1: ex_inf_of X,L and
A2: "/\" X,L in the carrier of S ; :: thesis: ( ex_inf_of X,S & "/\" X,S = "/\" X,L )
reconsider a = "/\" X,L as Element of S by A2;
consider a' being Element of L such that
A3: ( X is_>=_than a' & ( for b being Element of L st X is_>=_than b holds
b <= a' ) ) and
for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds
b <= c ) holds
c = a' by A1, Def8;
A4: a' = "/\" X,L by A1, A3, Def10;

A5: now

"/\" X,L is_<=_than X by A1, Def10;
hence a is_<=_than X by Th62; :: thesis: for b being Element of S st b is_<=_than X holds
b <= a
let b be Element of S; :: thesis: ( b is_<=_than X implies b <= a )
reconsider b' = b as Element of L by Th59;
assume b is_<=_than X ; :: thesis: b <= a
then b' is_<=_than X by Th63;
then b' <= "/\" X,L by A1, Def10;
hence b <= a by Th61; :: thesis: verum

end;

thus ex_inf_of X,S :: thesis: "/\" X,S = "/\" X,L

proof

take a ; :: according to YELLOW_0:def 8 :: thesis: ( X is_>=_than a & ( for b being Element of S st X is_>=_than b holds
b <= a ) & ( for c being Element of S st X is_>=_than c & ( for b being Element of S st X is_>=_than b holds
b <= c ) holds
c = a ) )
thus ( a is_<=_than X & ( for b being Element of S st b is_<=_than X holds
b <= a ) ) by A5; :: thesis: for c being Element of S st X is_>=_than c & ( for b being Element of S st X is_>=_than b holds
b <= c ) holds
c = a
let c be Element of S; :: thesis: ( X is_>=_than c & ( for b being Element of S st X is_>=_than b holds
b <= c ) implies c = a )
reconsider c' = c as Element of L by Th59;
assume X is_>=_than c ; :: thesis: ( ex b being Element of S st
( X is_>=_than b & not b <= c ) or c = a )
then A6: X is_>=_than c' by Th63;
assume for b being Element of S st X is_>=_than b holds
b <= c ; :: thesis: c = a
then A7: a <= c by A5;

now

let b be Element of L; :: thesis: ( X is_>=_than b implies b <= c' )
assume X is_>=_than b ; :: thesis: b <= c'
then ( b <= a' & a' <= c' ) by A3, A4, A7, Th60;
hence b <= c' by ORDERS_2:26; :: thesis: verum

end;

hence c = a by A1, A6, Def10; :: thesis: verum

end;

hence "/\" X,S = "/\" X,L by A5, Def10; :: thesis: verum