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