let L be non empty RelStr ; :: thesis: for x being Element of L holds
( x in PRIME (L opp ) iff x is co-prime )
let x be Element of L; :: thesis: ( x in PRIME (L opp ) iff x is co-prime )

hereby :: thesis: ( x is co-prime implies x in PRIME (L opp ) )

assume x in PRIME (L opp ) ; :: thesis: x is co-prime
then x ~ in PRIME (L opp ) by LATTICE3:def 6;
then x ~ is prime by WAYBEL_6:def 7;
hence x is co-prime by WAYBEL_6:def 8; :: thesis: verum

end;

assume x is co-prime ; :: thesis: x in PRIME (L opp )
then x ~ is prime by WAYBEL_6:def 8;
then x ~ in PRIME (L opp ) by WAYBEL_6:def 7;
hence x in PRIME (L opp ) by LATTICE3:def 6; :: thesis: verum