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

( \\/ (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