let C be FormalContext; :: thesis: [(phi C),(psi C)] is co-Galois
A1: LattPOSet (BooleLatt the carrier of C) = RelStr(# the carrier of (BooleLatt the carrier of C),(LattRel (BooleLatt the carrier of C)) #) by LATTICE3:def 2;
A2: LattPOSet (BooleLatt the carrier' of C) = RelStr(# the carrier of (BooleLatt the carrier' of C),(LattRel (BooleLatt the carrier' of C)) #) by LATTICE3:def 2;
A3: for x being Element of (BoolePoset the carrier of C)
for y being Element of (BoolePoset the carrier' of C) st x <= (psi C) . y holds
y <= (phi C) . x

proof

let x be Element of (BoolePoset the carrier of C); :: thesis: for y being Element of (BoolePoset the carrier' of C) st x <= (psi C) . y holds
y <= (phi C) . x
let y be Element of (BoolePoset the carrier' of C); :: thesis: ( x <= (psi C) . y implies y <= (phi C) . x )
assume x <= (psi C) . y ; :: thesis: y <= (phi C) . x
then [x,((psi C) . y)] in the InternalRel of (BoolePoset the carrier of C) by ORDERS_2:def 9;
then A4: [x,((psi C) . y)] in LattRel (BooleLatt the carrier of C) by A1, YELLOW_1:def 2;
reconsider x = x as Element of (BooleLatt the carrier of C) by A1, YELLOW_1:def 2;
reconsider y' = (psi C) . y as Element of (BooleLatt the carrier of C) by A1, YELLOW_1:def 2;
x [= y' by A4, FILTER_1:32;
then A5: x "\/" y' = y' by LATTICES:def 3;
reconsider x = x as Subset of the carrier of C by LATTICE3:def 1;
reconsider y' = y' as Subset of the carrier of C by LATTICE3:def 1;
A6: x c= y'

proof

for z being set st z in x holds
z in y' by A5, XBOOLE_0:def 3;
hence x c= y' by TARSKI:def 3; :: thesis: verum

end;

reconsider x = x, y' = y' as Subset of the carrier of C ;
reconsider y = y as Element of (BooleLatt the carrier' of C) by A2, YELLOW_1:def 2;
reconsider y = y as Subset of the carrier' of C by LATTICE3:def 1;
A7: (ObjectDerivation C) . y' c= (ObjectDerivation C) . x by A6, Th3;
A8: y c= (ObjectDerivation C) . ((AttributeDerivation C) . y) by Th6;
reconsider x = x as Element of (BoolePoset the carrier of C) ;
reconsider x' = (phi C) . x as Element of (BooleLatt the carrier' of C) by A2, YELLOW_1:def 2;
reconsider x' = x' as Subset of the carrier' of C by LATTICE3:def 1;
reconsider y = y as Element of (BooleLatt the carrier' of C) ;
reconsider x' = x' as Element of (BooleLatt the carrier' of C) ;
y "\/" x' = x' by A7, A8, XBOOLE_1:1, XBOOLE_1:12;
then y [= x' by LATTICES:def 3;
then [y,((phi C) . x)] in LattRel (BooleLatt the carrier' of C) by FILTER_1:32;
then [y,((phi C) . x)] in the InternalRel of (BoolePoset the carrier' of C) by A2, YELLOW_1:def 2;
hence y <= (phi C) . x by ORDERS_2:def 9; :: thesis: verum

end;

for x being Element of (BoolePoset the carrier of C)
for y being Element of (BoolePoset the carrier' of C) st y <= (phi C) . x holds
x <= (psi C) . y

proof

let x be Element of (BoolePoset the carrier of C); :: thesis: for y being Element of (BoolePoset the carrier' of C) st y <= (phi C) . x holds
x <= (psi C) . y
let y be Element of (BoolePoset the carrier' of C); :: thesis: ( y <= (phi C) . x implies x <= (psi C) . y )
assume y <= (phi C) . x ; :: thesis: x <= (psi C) . y
then [y,((phi C) . x)] in the InternalRel of (BoolePoset the carrier' of C) by ORDERS_2:def 9;
then A9: [y,((phi C) . x)] in LattRel (BooleLatt the carrier' of C) by A2, YELLOW_1:def 2;
reconsider y = y as Element of (BooleLatt the carrier' of C) by A2, YELLOW_1:def 2;
reconsider x' = (phi C) . x as Element of (BooleLatt the carrier' of C) by A2, YELLOW_1:def 2;
y [= x' by A9, FILTER_1:32;
then A10: y "\/" x' = x' by LATTICES:def 3;
reconsider y = y as Subset of the carrier' of C by LATTICE3:def 1;
reconsider x' = x' as Subset of the carrier' of C by LATTICE3:def 1;
A11: y c= x'

proof

for z being set st z in y holds
z in x' by A10, XBOOLE_0:def 3;
hence y c= x' by TARSKI:def 3; :: thesis: verum

end;

reconsider x = x as Element of (BooleLatt the carrier of C) by A1, YELLOW_1:def 2;
reconsider x = x as Subset of the carrier of C by LATTICE3:def 1;
A12: (AttributeDerivation C) . x' c= (AttributeDerivation C) . y by A11, Th4;
A13: x c= (AttributeDerivation C) . ((ObjectDerivation C) . x) by Th5;
reconsider y = y as Element of (BoolePoset the carrier' of C) ;
reconsider y' = (psi C) . y as Element of (BooleLatt the carrier of C) by A1, YELLOW_1:def 2;
reconsider y' = y' as Subset of the carrier of C by LATTICE3:def 1;
reconsider x = x as Subset of the carrier of C ;
reconsider x = x as Element of (BooleLatt the carrier of C) ;
reconsider y' = y' as Element of (BooleLatt the carrier of C) ;
x "\/" y' = y' by A12, A13, XBOOLE_1:1, XBOOLE_1:12;
then x [= y' by LATTICES:def 3;
then [x,((psi C) . y)] in LattRel (BooleLatt the carrier of C) by FILTER_1:32;
then [x,((psi C) . y)] in the InternalRel of (BoolePoset the carrier of C) by A1, YELLOW_1:def 2;
hence x <= (psi C) . y by ORDERS_2:def 9; :: thesis: verum

end;

hence [(phi C),(psi C)] is co-Galois by A3, Th13; :: thesis: verum