let L be non empty antisymmetric complete RelStr ; :: thesis: for F being Function holds
( \\/ F,L = //\ F,(L opp ) & //\ F,L = \\/ F,(L opp ) )
let F be Function; :: thesis: ( \\/ F,L = //\ F,(L opp ) & //\ F,L = \\/ F,(L opp ) )
A1: ( ex_sup_of rng F,L & ex_inf_of rng F,L ) by YELLOW_0:17;
thus \\/ F,L = "\/" (rng F),L by YELLOW_2:def 5
.= "/\" (rng F),(L opp ) by A1, Th12
.= //\ F,(L opp ) by YELLOW_2:def 6 ; :: thesis: //\ F,L = \\/ F,(L opp )
thus //\ F,L = "/\" (rng F),L by YELLOW_2:def 6
.= "\/" (rng F),(L opp ) by A1, Th13
.= \\/ F,(L opp ) by YELLOW_2:def 5 ; :: thesis: verum