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 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))
A2: ex_inf_of rng F,L by YELLOW_0:17;
thus //\ (F,L) = "/\" ((rng F),L) by YELLOW_2:def 6
.= "\/" ((rng F),(L opp)) by A2, Th13
.= \\/ (F,(L opp)) by YELLOW_2:def 5 ; :: thesis: verum