let L be non empty RelStr ; :: thesis: for X being set holds
( ( ex_sup_of X,L implies ex_sup_of X /\ the carrier of L,L ) & ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) & ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) & ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) )
let X be set ; :: thesis: ( ( ex_sup_of X,L implies ex_sup_of X /\ the carrier of L,L ) & ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) & ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) & ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) )
set Y = X /\ the carrier of L;
( ( for x being Element of L holds
( x is_<=_than X iff x is_<=_than X /\ the carrier of L ) ) & ( for x being Element of L holds
( x is_>=_than X iff x is_>=_than X /\ the carrier of L ) ) ) by Th5;
hence ( ( ex_sup_of X,L implies ex_sup_of X /\ the carrier of L,L ) & ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) & ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) & ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) ) by Th46, Th48; :: thesis: verum