let L be Lattice; :: thesis: for a, b being Element of L holds
( b in PseudoCocomplements a iff b "\/" a = Top L )
let a, b be Element of L; :: thesis: ( b in PseudoCocomplements a iff b "\/" a = Top L )

hereby :: thesis: ( b "\/" a = Top L implies b in PseudoCocomplements a )

assume b in PseudoCocomplements a ; :: thesis: b "\/" a = Top L
then consider x being Element of L such that
A1: ( b = x & a "\/" x = Top L ) ;
thus b "\/" a = Top L by A1; :: thesis: verum

end;

assume b "\/" a = Top L ; :: thesis: b in PseudoCocomplements a
hence b in PseudoCocomplements a ; :: thesis: verum