let C be FormalContext; [(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 y <= (phi C) . x holds
x <= (psi C) . y
proof
let x be
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) . ylet y be
Element of
(BoolePoset the carrier' of C);
( y <= (phi C) . x implies x <= (psi C) . y )
assume
y <= (phi C) . x
;
x <= (psi C) . y
then
[y,((phi C) . x)] in the
InternalRel of
(BoolePoset the carrier' of C)
by ORDERS_2:def 5;
then A4:
[y,((phi C) . x)] in LattRel (BooleLatt the carrier' of C)
by A1, YELLOW_1:def 2;
reconsider x9 =
(phi C) . x as
Element of
(BooleLatt the carrier' of C) by A1, YELLOW_1:def 2;
reconsider x =
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) by A1, YELLOW_1:def 2;
y [= x9
by A4, FILTER_1:31;
then A5:
y "\/" x9 = x9
by LATTICES:def 3;
reconsider x9 =
x9 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;
for
z being
object st
z in y holds
z in x9
by A5, XBOOLE_0:def 3;
then
y c= x9
;
then A6:
(AttributeDerivation C) . x9 c= (AttributeDerivation C) . y
by Th4;
reconsider y =
y as
Element of
(BoolePoset the carrier' of C) ;
reconsider y9 =
(psi C) . y as
Element of
(BooleLatt the carrier of C) by A2, YELLOW_1:def 2;
reconsider y9 =
y9 as
Subset of the
carrier of
C by LATTICE3:def 1;
reconsider y9 =
y9 as
Element of
(BooleLatt the carrier of C) ;
A7:
x c= (AttributeDerivation C) . ((ObjectDerivation C) . x)
by Th5;
reconsider x =
x as
Subset of the
carrier of
C ;
reconsider x =
x as
Element of
(BooleLatt the carrier of C) ;
x "\/" y9 = y9
by A6, A7, XBOOLE_1:1, XBOOLE_1:12;
then
x [= y9
by LATTICES:def 3;
then
[x,((psi C) . y)] in LattRel (BooleLatt the carrier of C)
by FILTER_1:31;
then
[x,((psi C) . y)] in the
InternalRel of
(BoolePoset the carrier of C)
by A2, YELLOW_1:def 2;
hence
x <= (psi C) . y
by ORDERS_2:def 5;
verum
end;
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);
for y being Element of (BoolePoset the carrier' of C) st x <= (psi C) . y holds
y <= (phi C) . xlet y be
Element of
(BoolePoset the carrier' of C);
( x <= (psi C) . y implies y <= (phi C) . x )
assume
x <= (psi C) . y
;
y <= (phi C) . x
then
[x,((psi C) . y)] in the
InternalRel of
(BoolePoset the carrier of C)
by ORDERS_2:def 5;
then A8:
[x,((psi C) . y)] in LattRel (BooleLatt the carrier of C)
by A2, YELLOW_1:def 2;
reconsider y9 =
(psi C) . y as
Element of
(BooleLatt the carrier of C) by A2, YELLOW_1:def 2;
reconsider y =
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
Element of
(BooleLatt the carrier of C) by A2, YELLOW_1:def 2;
x [= y9
by A8, FILTER_1:31;
then A9:
x "\/" y9 = y9
by LATTICES:def 3;
reconsider y9 =
y9 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;
for
z being
object st
z in x holds
z in y9
by A9, XBOOLE_0:def 3;
then A10:
x c= y9
;
reconsider x =
x,
y9 =
y9 as
Subset of the
carrier of
C ;
A11:
(ObjectDerivation C) . y9 c= (ObjectDerivation C) . x
by A10, Th3;
reconsider x =
x as
Element of
(BoolePoset the carrier of C) ;
reconsider x9 =
(phi C) . x as
Element of
(BooleLatt the carrier' of C) by A1, YELLOW_1:def 2;
reconsider x9 =
x9 as
Subset of the
carrier' of
C by LATTICE3:def 1;
reconsider x9 =
x9 as
Element of
(BooleLatt the carrier' of C) ;
A12:
y c= (ObjectDerivation C) . ((AttributeDerivation C) . y)
by Th6;
reconsider y =
y as
Element of
(BooleLatt the carrier' of C) ;
y "\/" x9 = x9
by A11, A12, XBOOLE_1:1, XBOOLE_1:12;
then
y [= x9
by LATTICES:def 3;
then
[y,((phi C) . x)] in LattRel (BooleLatt the carrier' of C)
by FILTER_1:31;
then
[y,((phi C) . x)] in the
InternalRel of
(BoolePoset the carrier' of C)
by A1, YELLOW_1:def 2;
hence
y <= (phi C) . x
by ORDERS_2:def 5;
verum
end;
hence
[(phi C),(psi C)] is co-Galois
by A3, Th12; verum